$\forall$$T$:Type, $l_{1}$, $l_{2}$, $l_{3}$:($T$ List). $l_{1}$ $\leq$ $l_{2}$ @ $l_{3}$ $\Rightarrow$ ($\parallel$$l_{1}$$\parallel$ $\leq$ $\parallel$$l_{2}$$\parallel$) $\Rightarrow$ $l_{1}$ $\leq$ $l_{2}$